Inference at * 1 
Iof proof for Lemma bool cases:



1. b : 
  (b = tt)  (b = ff) 

latex

 by BoolInd 1 

latex

 1: 

 1: (no hyps)
 1:   (tt = tt)  (tt = ff)
 2: 

 2: (no hyps)
 2:   (ff = tt)  (ff = ff)
 .

Definitions

t  T, Unit, , , ff, tt